#pragma once
 #include "ArrowType.h"
#include "AbstractType.h"
// Term command target

#define  _APPLICATIONTERM(Ter)  static_cast<const ApplicationTerm&>(Ter)
#define  _ABSTRACTTERM(Ter)  static_cast<const AbstractTerm&>(Ter)
#define  _ABSTRACTTYPETERM(Ter)  static_cast<const AbstractTypeTerm&>(Ter)


class TermXception : public TokenXception{
public:
			TermXception(string err):TokenXception(string("TypeXception")+err){};
};


struct TermIterator;
class Term : public Token
{
public:
	typedef TermXception exception;
	typedef const TermXception& const_exception;

	typedef Term* pointer;
	typedef const Term* const_pointer;
	
	typedef Term& reference;
	typedef const Term& const_reference;
	
	typedef TermIterator iterator;
	typedef const TermIterator const_iterator;

protected:
	Type::pointer m_Type;
	void assignType(Type::const_reference);
	

public:
	virtual bool isAbstractTerm() const{return false;};
	virtual bool isTermVariable() const{return false;};
	virtual bool isApplicationTerm() const{return false;};
	virtual bool isAbstractTypeTerm() const{return false;};
	virtual bool isRedex() const{return false;};
	

public:
	Term(const Type&, const string& = "");
	Term(const Term&);
	virtual ~Term();

public:
	Type::const_reference getType() const{return *m_Type;};
	void normalizeType();
	void setTypeSyntax(string);

public:
//Token overides  
	bool isTerm()const{return true;};
	bool isType() const{return false;};
	bool isReducible() const;	   
	string view() const;
	bool operator==(Token::const_reference To);	 
	Token::pointer replaceAll(Token::const_reference, Token::const_reference) const;
	COUNTER complexity() const;

public:
	virtual bool TypeOccursinFreeVariable(Type::const_reference) const=0;

public:
	static Type::pointer ResolveType(Type::const_reference, Type::const_reference);
	
};


struct TermIterator{
		typedef			TermIterator*				pointer;
		typedef			const TermIterator*		const_pointer;
		typedef			TermIterator&				reference;
		typedef			const TermIterator&	const_reference;
		typedef			pointer						iterator;
		typedef			const_pointer				const_iterator;

		Term::pointer ptr;
		TermIterator(Term* TePtr):ptr(TePtr){};
		TermIterator(const TermIterator& TeIt):ptr(static_cast<Term::pointer>(TeIt.ptr->clone())){};
		~TermIterator(){delete ptr;};
		bool operator==(const TermIterator& TeIt) const{return (ptr->operator ==(*(TeIt.ptr)));};
	};

struct ltTermIterator{
	bool operator()(TermIterator S1, TermIterator S2) const{
		if((S1.ptr)->complexity() < (S2.ptr)->complexity()) return true;
		return !(S1==S2) ;
		//two different terms, same complexity?

		};
};








